fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
↳ QTRS
↳ Overlay + Local Confluence
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
FIB1(X, Y) → ADD(X, Y)
ADD(s(X), Y) → ADD(X, Y)
SEL(s(N), cons(X, XS)) → SEL(N, XS)
FIB(N) → SEL(N, fib1(s(0), s(0)))
FIB1(X, Y) → FIB1(Y, add(X, Y))
FIB(N) → FIB1(s(0), s(0))
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
FIB1(X, Y) → ADD(X, Y)
ADD(s(X), Y) → ADD(X, Y)
SEL(s(N), cons(X, XS)) → SEL(N, XS)
FIB(N) → SEL(N, fib1(s(0), s(0)))
FIB1(X, Y) → FIB1(Y, add(X, Y))
FIB(N) → FIB1(s(0), s(0))
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
FIB1(X, Y) → ADD(X, Y)
ADD(s(X), Y) → ADD(X, Y)
SEL(s(N), cons(X, XS)) → SEL(N, XS)
FIB(N) → SEL(N, fib1(s(0), s(0)))
FIB1(X, Y) → FIB1(Y, add(X, Y))
FIB(N) → FIB1(s(0), s(0))
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
SEL(s(N), cons(X, XS)) → SEL(N, XS)
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SEL(s(N), cons(X, XS)) → SEL(N, XS)
trivial
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ADD(s(X), Y) → ADD(X, Y)
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ADD(s(X), Y) → ADD(X, Y)
trivial
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
FIB1(X, Y) → FIB1(Y, add(X, Y))
fib(N) → sel(N, fib1(s(0), s(0)))
fib1(X, Y) → cons(X, fib1(Y, add(X, Y)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
sel(0, cons(X, XS)) → X
sel(s(N), cons(X, XS)) → sel(N, XS)
fib(x0)
fib1(x0, x1)
add(0, x0)
add(s(x0), x1)
sel(0, cons(x0, x1))
sel(s(x0), cons(x1, x2))